PROOF ONE 

1:	F←(λ X) ¬ X X BY DEF(F,(λ X) ¬ X X) ASSUMING (1) 

2:	F F BY ASSUMPTION 

3:	((λ X) ¬ X X) F BY REPL(2,1,1) ASSUMING (2 1) 

4:	((λ X) ¬ X X) F=¬ F F BY LC((λ X) ¬ X X,F) 

5:	¬ F F BY REPL(3,4,1) ASSUMING (1 2) 

6:	FALSE BY NE(2,5) ASSUMING (1 2) 

7:	F F⊃FALSE BY DED(6,2) ASSUMING (1) 

8:	¬ F F BY NI 7 ASSUMING (1) 

9:	¬ ((λ X) ¬ X X) F BY REPL(8,1,1) ASSUMING (1) 

10:	¬ ¬ F F BY REPL(9,4,1) ASSUMING (1) 

11:	F F BY DNE 10 ASSUMING (1) 

12:	FALSE BY NE(8,11) ASSUMING (1) 

13:	FALSE BY ELIM(12,1)